\begin{tabbing}
lpath($p$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\forall$$i$:\{0..($\parallel$$p$$\parallel$ {-} 1)$^{-}$\}.\+
\\[0ex]destination($p$[$i$]) = source($p$[($i$+1)]) $\in$ Id \& ($\neg$($p$[($i$+1)] = lnk{-}inv($p$[$i$]) $\in$ IdLnk))
\-
\end{tabbing}